Nuprl Lemma : mapl_wf
0,22
postcript
pdf
A
,
B
:Type,
L
:
A
List,
f
:({
a
:
A
| (
a
L
) }
B
). mapl(
f
;
L
)
B
List
latex
Definitions
mapl(
f
;
l
)
Lemmas
map-wf2
origin
A, B:Type, L:A List, f:({a:A| (a 
L) }
B). mapl(f;L) B List A, B:Type, L:A List, f:({a:A| (a L) }B). mapl(f;L) B List